i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), snd:msg-spec(ds; da), upd:update-spec(ds; da),
T:Type, ks:(Knd List), a:((k:{k:Knd| (k  ks)} decl-state(ds)ma-valtype(da; k)T)),
x:Id.
((fpf-dom(id-deq; x; ds)))
 update-spec-decl(upd; ds)
 (k:Knd. (k  ks)  (fpf-dom(Kind-deq; k; da)))
 R-compat{i:l}
 R-compat(ecl-machine2(i; ds; da; x; T; ks; a; upd); ecl-machine3(ds; da; x; T; ks; a; snd)) 

latex

Definitions	prop{i:l}, ff, tt, top, x,y. t(x;y), x. t(x), t.2, t.1, fpf-cap(f; eq; x; z), if b then t else f fi , t  T, P  Q, x:A. B(x), decl-state(ds), False, P  Q, P  Q, Unit, x(s), x(s1,s2), A, , update-spec(ds; da),
Lemmas	assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, fpf-dom wf, eqof eq btrue, fpf-cap-single, fpf-trivial-subtype-top, id-deq wf, fpf-join-cap-sq, fpf-cap-join-subtype, subtype rel self, top wf, fpf-single wf, fpf-join wf, fpf-cap wf, subtype rel dep function, fpf-ap wf, list accum wf